(*
 * Copyright (c) 2009, Palle Raabjerg
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   * Redistributions of source code must retain the above copyright notice,
 *     this list of conditions and the following disclaimer.
 *   * Redistributions in binary form must reproduce the above copyright notice,
 *     this list of conditions and the following disclaimer in the documentation
 *     and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 *)

(** Generate ALFP formula from a constraint formula. *)

open Alfp
open Axioms;;

module SMap = Map.Make(String);;

(** Get proper name of message
    @param msg Message

    @return String indicating proper name
*)
let propername_of_msg msg =
  Spitree.string_of_msg msg

(** Get proper name of environment
    @param env Environment

    @return String indicating proper name
*)
let propername_of_env env =
  Constraints.string_of_env env
  (*Spitree.string_of_env env*)

(** Generate ALFP formula from environment
    @param env Environment

    @return ALFP formula
*)
let formula_of_env env =
  let e = propername_of_env env in
  let rec assemble env =
    match env with
      | Constraints.Type(x, t)::restenv ->
	  ClAnd(CPredicate(envrel, constlist [x; t; e]),
		assemble restenv)
      | Constraints.UnType(x)::restenv -> assemble restenv
      | Constraints.Effect(reso)::restenv ->
	  let rec formula_of_reso reso =
	    (match reso with
	       | Constraints.Reso(l, m) -> CPredicate(envrel, constlist [l; propername_of_msg m; e])
	       | Constraints.RPair(r1, r2) -> ClAnd(formula_of_reso r1,
					formula_of_reso r2)
	       | Constraints.Empty -> Truth)
	  in
	    ClAnd(formula_of_reso reso, assemble restenv)
      | [] -> Truth
  in
    assemble env

(** Generate ALFP formula from list of environments
    @param env Environment list

    @return ALFP formula
*)
let rec formula_of_envlist envlist =
  match envlist with
    | env::restenvs ->
	ClAnd(formula_of_env env, formula_of_envlist restenvs)
    | [] -> Truth

(** Extract domain from environment
    @param env Environment

    @return List of names indicating the domain of env
*)
let listdom env =
  List.fold_left (fun dlist typ ->
		    match typ with
		      | Constraints.Type(x, _) -> x::dlist
		      | Constraints.UnType(x) -> x::dlist
		      | _ -> dlist
		 ) [] env

(** Generate ALFP formula from list of environments
    @param envlist Environment list

    @return ALFP formula
*)
let domformula envlist =
  let domains =
    List.map (fun env ->
		listdom env
	     ) envlist
  in
  let formula_list =
    List.concat
      (List.map2 (fun env domain ->
		    List.map (fun name ->
				CPredicate(domrel, constlist [name; Constraints.string_of_env env])
			     ) domain
		 ) envlist domains)
  in
    List.fold_left (fun accum_formula formula ->
		      ClAnd(accum_formula, formula)
		   ) (List.hd formula_list) (List.tl formula_list)

(** Create a mapping from relations to ranks, based on the list found in the Axioms module *)
let rank = List.fold_left (fun map_accum reltuple ->
			     let relation, rank = reltuple in
			       SMap.add relation rank map_accum
			  ) SMap.empty ranklist


exception UnmatchedRank of string;;

(** Stratify alfp formulae according to specified ranks
    @param alfp_cl ALFP formula to stratify

    @return Stratified ALFP formula
*)
let stratify alfp_cl =
  let rec rank_of_cl cl =
    match cl with
      | CPredicate(rel, _) ->
	  print_endline rel;
	  SMap.find rel rank
      | Truth -> 0   (* Not a true/false value! 0 is used to indicate to the rank comparison below
		      * that truth statements have no rank. *)
      | (ClAnd(cl1, cl2) | CommentClAnd(_, cl1, cl2)) ->
	  let rank1, rank2 = (rank_of_cl cl1), (rank_of_cl cl2) in
	    (match (rank1, rank2) with
	       | (0, _) -> rank2
	       | (_, 0) -> rank1
	       | (_, _) ->
		   if (rank1 = rank2) || (rank1 = 0) || (rank2 = 0) then
		     rank1
		   else
		     raise (UnmatchedRank (" " ^ (string_of_cl cl1) ^ "   " ^ (string_of_cl cl2) ^ "  - Ranks of the consequence of a Horn clause must match")))
      | Leadsto(_, cl) ->
	  rank_of_cl cl
      | Forall(_, cl) ->
	  rank_of_cl cl
  in
  let rec annotate clause =
    match clause with
      | CPredicate(rel, _) ->
	  [(rank_of_cl clause, clause)]
      | Truth -> [(rank_of_cl Truth, Truth)]
      | (ClAnd(cl1, cl2) | CommentClAnd(_, cl1, cl2)) ->
	  List.append (annotate cl1) (annotate cl2)
      | Leadsto(_, cl) ->
	  [(rank_of_cl cl, clause)]
      | Forall(_, cl) ->
	  let (rank, _) = List.hd (annotate cl) in
	    [(rank, clause)]
  in
  let annotated_list = annotate alfp_cl in
  let sorted_annotation = List.sort (fun el1 el2 ->
				       let (rank1, _) = el1 in
				       let (rank2, _) = el2 in
					 compare rank1 rank2
				    ) annotated_list
  in
  let (_, stratified_list) = List.split sorted_annotation in
    List.fold_left (fun accum_cl cl ->
		      ClAnd(accum_cl, cl)
		   ) Truth stratified_list

(** Function for debugging. Prints out the commented version of a list-based conjunction
    @param conj List-based conjunction containing comments
*)
let print_commented_conjunction conj =
  List.iter (fun element ->
	       match element with
		 | Clause(cl) ->
		     print_endline ((string_of_cl cl) ^ "\n")
		 | Comment(str) ->
		     print_endline ("\n" ^ str ^ "\n")
	    ) conj

(* - Encodings - *)

(** Generate ALFP formula from message term
    @param msg Message

    @return ALFP formula
*)
let rec alfp_of_msg msg =
  let n = propername_of_msg msg in
    (n,
     match msg with
       | Spitree.MPair(msg1, msg2) ->
	   let m1, psi1 = alfp_of_msg msg1 in
	   let m2, psi2 = alfp_of_msg msg2 in
	     ClAnd(CPredicate(tpairrel, [Const(n); Const(m1); Const(m2)]),
		   ClAnd(psi1, psi2))
       | Spitree.Encr(msg1, msg2) ->
	   let m1, psi1 = alfp_of_msg msg1 in
	   let m2, psi2 = alfp_of_msg msg2 in
	     ClAnd(CPredicate(encrel, [Const(n); Const(m1); Const(m2)]),
		   ClAnd(psi1, psi2))
       | Spitree.Name(_) ->
	   CPredicate(namerel, [Const(n)])
       | Spitree.Ok ->
	   CPredicate(tokrel, [Const(n)])
    )

(* let msg_equality m n =
 * Hang on. Where on earth are we using message equality? *)

(* Type constraints *)
(** Raised if an attempt is made to translate constraints containing constructions unsupported by ALFP *)
exception UnsupportedByALFP of string;;

(** Raised if a translation might be possible, but is not implemented *)
exception NotImplemented of string;;

(** Generate ALFP clause from a type constraint
    @param typeconstraint Type constraint

    @return ALFP formula

    @raise UnsupportedByALFP On negated predicates
*)
let rec clause_of_typeconstraint typeconstraint =
  match typeconstraint with
    | Constraints.Equal(t, basetype) ->
	(match basetype with
	   | Constraints.Key(t1) -> CPredicate(keyrel, [Const(t); Const(t1)])
	   | Constraints.Pair(x, t1, t2) -> CPredicate(pairrel, [Const(t); Const(x); Const(t1); Const(t2)])
	   | Constraints.Ch(t1) -> CPredicate(chrel, [Const(t); Const(t1)])
	   | Constraints.Un -> CPredicate(unrel, [Const(t)])
	   | Constraints.Ok(r) -> CPredicate(okrel, [Const(t); Const(r)])
	   | Constraints.Abstraction(u, m, x) -> ClAnd(CPredicate(teqrel, constlist [t; u]),
						       CPredicate(absrel, constlist [t; u; propername_of_msg m; x]))
	   | Constraints.Application(u, n) -> CPredicate(apprel, constlist [t; u; propername_of_msg n])
	)
    | Constraints.MayEqual(t, basetype) ->
	(match basetype with
	   | Constraints.Key(t1) -> CPredicate(keyrel ^ maypf, [Const(t); Const(t1)])
	   | Constraints.Pair(x, t1, t2) -> CPredicate(pairrel ^ maypf, [Const(t); Const(x); Const(t1); Const(t2)])
	   | Constraints.Ch(t1) -> CPredicate(chrel ^ maypf, [Const(t); Const(t1)])
	   | Constraints.Un -> CPredicate(unrel ^ maypf, [Const(t)])
	   | Constraints.Ok(r) -> CPredicate(okrel ^ maypf, [Const(t); Const(r)])
	   | Constraints.Abstraction(u, m, x) -> ClAnd(CPredicate(teqrel, constlist [t; u]),
							CPredicate(absrel ^ maypf, constlist [t; u; propername_of_msg m; x]))
	   | Constraints.Application(u, n) -> CPredicate(apprel ^ maypf, constlist [t; u; propername_of_msg n])
	)
    | Constraints.Generative(t) -> CPredicate(genrel, [Const(t)])
    | Constraints.NotGenerative(t) -> raise (UnsupportedByALFP "Negated predicates can only occur in preconditions")
    | Constraints.HasType(x, t) -> CPredicate(typrel, constlist [x; t])
    | Constraints.Fail -> CPredicate(failrel, [Const("Something failed!")])
(*    | Constraints.NotFN(_, _) -> raise (UnsupportedByALFP "Negated predicates can only occur in preconditions")*)
    | Constraints.NotUn(_) -> raise (UnsupportedByALFP "Negated predicates can only occur in preconditions")
;;

(** Generate ALFP precondition from a type constraint
    @param typeconstraint Type constraint

    @return ALFP precondition

    @raise NotImplemented On Fail relations, as they are not used in preconditions
*)
let rec precondition_of_typeconstraint typeconstraint =
  match typeconstraint with
    | Constraints.Equal(t, basetype) ->
	(match basetype with
	   | Constraints.Key(t1) -> PPredicate(keyrel, [Const(t); Const(t1)])
	   | Constraints.Pair(x, t1, t2) -> PPredicate(pairrel, [Const(t); Const(x); Const(t1); Const(t2)])
	   | Constraints.Ch(t1) -> PPredicate(chrel, [Const(t); Const(t1)])
	   | Constraints.Un -> PPredicate(unrel, [Const(t)])
	   | Constraints.Ok(r) -> PPredicate(okrel, [Const(t); Const(r)])
	   | Constraints.Abstraction(u, m, x) -> PPredicate(absrel, constlist [t; u; propername_of_msg m; x])
	   | Constraints.Application(u, n) -> PPredicate(apprel, constlist [t; u; propername_of_msg n])
	)
    | Constraints.MayEqual(t, basetype) ->
	(match basetype with
	   | Constraints.Key(t1) -> PPredicate(keyrel ^ maypf, [Const(t); Const(t1)])
	   | Constraints.Pair(x, t1, t2) -> PPredicate(pairrel ^ maypf, [Const(t); Const(x); Const(t1); Const(t2)])
	   | Constraints.Ch(t1) -> PPredicate(chrel ^ maypf, [Const(t); Const(t1)])
	   | Constraints.Un -> PPredicate(unrel ^ maypf, [Const(t)])
	   | Constraints.Ok(r) -> PPredicate(okrel ^ maypf, [Const(t); Const(r)])
	   | Constraints.Abstraction(u, m, x) -> PPredicate(absrel ^ maypf, constlist [t; u; propername_of_msg m; x])
	   | Constraints.Application(u, n) -> PPredicate(apprel ^ maypf, constlist [t; u; propername_of_msg n])
	)
    | Constraints.Generative(t) -> PPredicate(genrel, [Const(t)])
    | Constraints.NotGenerative(t) -> NegPredicate(genrel, [Const(t)])
    | Constraints.HasType(x, t) -> PPredicate(typrel, constlist [x; t])
    | Constraints.Fail -> raise (NotImplemented "We only use Fail as the final relation in the final stratum. We never use it in a precondition")
(*    | Constraints.NotFN(x, p) -> raise (NotImplemented "We need to somehow determine the free names of a process.")*)
    | Constraints.NotUn(t) -> NegPredicate(teqrel, constlist [t; "Un"]) (* Might be wrong *)
;;

(** Generate ALFP formula from an environment constraint
    @param envconstraint Environment constraint

    @return ALFP formula
*)
let clause_of_envconstraint envconstraint =
  let namesindom propername env =
    let e = propername_of_env env in
      Leadsto(Exists("n",
		     PreAnd(PPredicate(fnrel, [Var("n"); Const(propername)]),
			    NegPredicate(domrel, [Var("n"); Const(e)]))),
	      CPredicate(failrel, [Const("Free names of " ^ propername ^ " not in environment " ^ e)])
	     )
  in
    match envconstraint with
      | Constraints.NotInDom(name, env) ->
	  Leadsto(PPredicate(domrel, constlist [name; propername_of_env env]),
		  CPredicate(failrel, [Const("Restricted name must not be in the environment of the restriction")]))
      | Constraints.NamesInDom(msg, env) ->
	  let m = propername_of_msg msg in
	    namesindom m env
      | Constraints.WellFormed(env) ->
	  let rec wf env =
	    (match env with
	       | [] -> Truth
	       | Constraints.Type(x, tvar)::restenv ->
		   let name_restenv = propername_of_env restenv in
		     ClAnd(wf restenv,
			   ClAnd(Leadsto(PPredicate(domrel, constlist [x; name_restenv]),
					 CPredicate(failrel, [Const("Environment is not well-formed: " ^ (Constraints.string_of_env env))])),
				 namesindom tvar restenv))
	       | Constraints.UnType(x)::restenv ->
		   let name_restenv = propername_of_env restenv in
		     ClAnd(wf restenv,
			   Leadsto(PPredicate(domrel, constlist [x; name_restenv]),
				   CPredicate(failrel, [Const("Environment is not well-formed: " ^ (Constraints.string_of_env env))]))
			  )
	       | Constraints.Effect(s)::restenv ->
		   ClAnd(wf restenv,
			 namesindom (Constraints.string_of_reso s) restenv)
	    )
	  in
	    wf env

(* The next two functions are the main functions for translating
 * constraints to ALFP formulae. The functions illustrate a certain
 * loss of expressive power compared to the original constraints.
 * But if all goes well, we should not have overstepped these boundaries
 * during constraint generation or the ALFP encoding. *)
(** Main function for translating constraints to ALFP preconditions
    @param formula Constraint formula

    @return ALFP precondition

    @raise UnsupportedByALFP On constructions that cannot be translated
    @raise NotImplemented On comments, as they should not occur in preconditions
*)
let rec precondition_of_formula formula =
  match formula with
    | Constraints.TypeC(constr) -> precondition_of_typeconstraint constr
    | Constraints.EnvC(constr) -> raise (UnsupportedByALFP "Environment constraints are assertions and should not be in a precondition.")
    | Constraints.EffectC(constr) -> raise (UnsupportedByALFP "ALFP effect constraint generation not implemented yet.")
    | Constraints.And(pre1, pre2) -> PreAnd(precondition_of_formula pre1, precondition_of_formula pre2)
    | Constraints.Conjunction(pre::[]) -> precondition_of_formula pre
    | Constraints.Conjunction(pre::rest) -> PreAnd(precondition_of_formula pre, precondition_of_formula (Constraints.Conjunction(rest)))
    | Constraints.Conjunction([]) -> raise (UnsupportedByALFP "Precondition cannot be empty")
    | Constraints.CommentConjunction(_, _) -> raise (NotImplemented "We do not give comments in preconditions")
    | Constraints.Or(pre1, pre2) -> Or(precondition_of_formula pre1, precondition_of_formula pre2)
    | Constraints.Leadsto(pre, cl) -> raise (UnsupportedByALFP "Horn clauses are not allowed in ALFP preconditions")
    | Constraints.Forall(x, cl) -> raise (UnsupportedByALFP "Quantification should happen over whole clauses, not just preconditions.")
    | Constraints.True -> raise (UnsupportedByALFP "Truth statements may only occur as a clause")

(** Main function for translating constraints to ALFP formulae
    @param formula Constraint formula

    @return ALFP formula

    @raise UnsupportedByALFP On disjunctions, as they cannot occur outside preconditions in ALFP
*)
let rec clause_of_formula formula =
  match formula with
    | Constraints.TypeC(constr) -> clause_of_typeconstraint constr
    | Constraints.EnvC(constr) -> clause_of_envconstraint constr
    | Constraints.EffectC(constr) -> CPredicate(failrel, [Const("ALFP effect constraint generation not implemented yet.")])
    | Constraints.And(cl1, cl2) -> ClAnd(clause_of_formula cl1, clause_of_formula cl2)
    | Constraints.Conjunction(cl::[]) -> clause_of_formula cl
    | Constraints.Conjunction(cl::rest) -> ClAnd(clause_of_formula cl, clause_of_formula (Constraints.Conjunction(rest)))
    | Constraints.Conjunction([]) -> Truth
    | Constraints.CommentConjunction(com, cl::rest) ->
	CommentClAnd(com, clause_of_formula cl, clause_of_formula (Constraints.Conjunction(rest)))
    | Constraints.CommentConjunction(com, []) -> Truth
    | Constraints.Or(cl1, cl2) -> raise (UnsupportedByALFP "Disjunction is only possible in preconditions!")
    | Constraints.Leadsto(pre, cl) -> Leadsto(precondition_of_formula pre, clause_of_formula cl)
    | Constraints.Forall(x, cl) -> Forall(x, clause_of_formula cl)
    | Constraints.True -> Truth
;;

